(0) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
subst(x, a, App(e1, e2)) → mkapp(subst(x, a, e1), subst(x, a, e2))
subst(x, a, Lam(var, exp)) → subst[True][Ite](eqTerm(x, V(var)), x, a, Lam(var, exp))
red(App(e1, e2)) → red[Let](App(e1, e2), red(e1))
red(Lam(int, term)) → Lam(int, term)
subst(x, a, V(int)) → subst[Ite](eqTerm(x, V(int)), x, a, V(int))
red(V(int)) → V(int)
eqTerm(App(t11, t12), App(t21, t22)) → and(eqTerm(t11, t21), eqTerm(t12, t22))
eqTerm(App(t11, t12), Lam(i2, l2)) → False
eqTerm(App(t11, t12), V(v2)) → False
eqTerm(Lam(i1, l1), App(t21, t22)) → False
eqTerm(Lam(i1, l1), Lam(i2, l2)) → and(!EQ(i1, i2), eqTerm(l1, l2))
eqTerm(Lam(i1, l1), V(v2)) → False
eqTerm(V(v1), App(t21, t22)) → False
eqTerm(V(v1), Lam(i2, l2)) → False
eqTerm(V(v1), V(v2)) → !EQ(v1, v2)
mklam(V(name), e) → Lam(name, e)
lamvar(Lam(var, exp)) → V(var)
lambody(Lam(var, exp)) → exp
isvar(App(t1, t2)) → False
isvar(Lam(int, term)) → False
isvar(V(int)) → True
islam(App(t1, t2)) → False
islam(Lam(int, term)) → True
islam(V(int)) → False
appe2(App(e1, e2)) → e2
appe1(App(e1, e2)) → e1
mkapp(e1, e2) → App(e1, e2)
lambdaint(e) → red(e)
The (relative) TRS S consists of the following rules:
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0, S(y)) → False
!EQ(S(x), 0) → False
!EQ(0, 0) → True
red[Let][Let](e, Lam(var, exp), a) → red(subst(V(var), a, exp))
subst[True][Ite](False, x, a, Lam(var, exp)) → mklam(V(var), subst(x, a, exp))
red[Let][Let](e, App(t1, t2), e2) → App(App(t1, t2), e2)
red[Let][Let](e, V(int), e2) → App(V(int), e2)
red[Let](App(e1, e2), f) → red[Let][Let](App(e1, e2), f, red(e2))
subst[True][Ite](True, x, a, e) → e
subst[Ite](False, x, a, e) → e
subst[Ite](True, x, a, e) → a
Rewrite Strategy: INNERMOST
(1) RenamingProof (EQUIVALENT transformation)
Renamed function symbols to avoid clashes with predefined symbol.
(2) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
subst(x, a, App(e1, e2)) → mkapp(subst(x, a, e1), subst(x, a, e2))
subst(x, a, Lam(var, exp)) → subst[True][Ite](eqTerm(x, V(var)), x, a, Lam(var, exp))
red(App(e1, e2)) → red[Let](App(e1, e2), red(e1))
red(Lam(int, term)) → Lam(int, term)
subst(x, a, V(int)) → subst[Ite](eqTerm(x, V(int)), x, a, V(int))
red(V(int)) → V(int)
eqTerm(App(t11, t12), App(t21, t22)) → and(eqTerm(t11, t21), eqTerm(t12, t22))
eqTerm(App(t11, t12), Lam(i2, l2)) → False
eqTerm(App(t11, t12), V(v2)) → False
eqTerm(Lam(i1, l1), App(t21, t22)) → False
eqTerm(Lam(i1, l1), Lam(i2, l2)) → and(!EQ(i1, i2), eqTerm(l1, l2))
eqTerm(Lam(i1, l1), V(v2)) → False
eqTerm(V(v1), App(t21, t22)) → False
eqTerm(V(v1), Lam(i2, l2)) → False
eqTerm(V(v1), V(v2)) → !EQ(v1, v2)
mklam(V(name), e) → Lam(name, e)
lamvar(Lam(var, exp)) → V(var)
lambody(Lam(var, exp)) → exp
isvar(App(t1, t2)) → False
isvar(Lam(int, term)) → False
isvar(V(int)) → True
islam(App(t1, t2)) → False
islam(Lam(int, term)) → True
islam(V(int)) → False
appe2(App(e1, e2)) → e2
appe1(App(e1, e2)) → e1
mkapp(e1, e2) → App(e1, e2)
lambdaint(e) → red(e)
The (relative) TRS S consists of the following rules:
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
red[Let][Let](e, Lam(var, exp), a) → red(subst(V(var), a, exp))
subst[True][Ite](False, x, a, Lam(var, exp)) → mklam(V(var), subst(x, a, exp))
red[Let][Let](e, App(t1, t2), e2) → App(App(t1, t2), e2)
red[Let][Let](e, V(int), e2) → App(V(int), e2)
red[Let](App(e1, e2), f) → red[Let][Let](App(e1, e2), f, red(e2))
subst[True][Ite](True, x, a, e) → e
subst[Ite](False, x, a, e) → e
subst[Ite](True, x, a, e) → a
Rewrite Strategy: INNERMOST
(3) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)
Infered types.
(4) Obligation:
Innermost TRS:
Rules:
subst(x, a, App(e1, e2)) → mkapp(subst(x, a, e1), subst(x, a, e2))
subst(x, a, Lam(var, exp)) → subst[True][Ite](eqTerm(x, V(var)), x, a, Lam(var, exp))
red(App(e1, e2)) → red[Let](App(e1, e2), red(e1))
red(Lam(int, term)) → Lam(int, term)
subst(x, a, V(int)) → subst[Ite](eqTerm(x, V(int)), x, a, V(int))
red(V(int)) → V(int)
eqTerm(App(t11, t12), App(t21, t22)) → and(eqTerm(t11, t21), eqTerm(t12, t22))
eqTerm(App(t11, t12), Lam(i2, l2)) → False
eqTerm(App(t11, t12), V(v2)) → False
eqTerm(Lam(i1, l1), App(t21, t22)) → False
eqTerm(Lam(i1, l1), Lam(i2, l2)) → and(!EQ(i1, i2), eqTerm(l1, l2))
eqTerm(Lam(i1, l1), V(v2)) → False
eqTerm(V(v1), App(t21, t22)) → False
eqTerm(V(v1), Lam(i2, l2)) → False
eqTerm(V(v1), V(v2)) → !EQ(v1, v2)
mklam(V(name), e) → Lam(name, e)
lamvar(Lam(var, exp)) → V(var)
lambody(Lam(var, exp)) → exp
isvar(App(t1, t2)) → False
isvar(Lam(int, term)) → False
isvar(V(int)) → True
islam(App(t1, t2)) → False
islam(Lam(int, term)) → True
islam(V(int)) → False
appe2(App(e1, e2)) → e2
appe1(App(e1, e2)) → e1
mkapp(e1, e2) → App(e1, e2)
lambdaint(e) → red(e)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
red[Let][Let](e, Lam(var, exp), a) → red(subst(V(var), a, exp))
subst[True][Ite](False, x, a, Lam(var, exp)) → mklam(V(var), subst(x, a, exp))
red[Let][Let](e, App(t1, t2), e2) → App(App(t1, t2), e2)
red[Let][Let](e, V(int), e2) → App(V(int), e2)
red[Let](App(e1, e2), f) → red[Let][Let](App(e1, e2), f, red(e2))
subst[True][Ite](True, x, a, e) → e
subst[Ite](False, x, a, e) → e
subst[Ite](True, x, a, e) → a
Types:
subst :: App:Lam:V → App:Lam:V → App:Lam:V → App:Lam:V
App :: App:Lam:V → App:Lam:V → App:Lam:V
mkapp :: App:Lam:V → App:Lam:V → App:Lam:V
Lam :: S:0' → App:Lam:V → App:Lam:V
subst[True][Ite] :: False:True → App:Lam:V → App:Lam:V → App:Lam:V → App:Lam:V
eqTerm :: App:Lam:V → App:Lam:V → False:True
V :: S:0' → App:Lam:V
red :: App:Lam:V → App:Lam:V
red[Let] :: App:Lam:V → App:Lam:V → App:Lam:V
subst[Ite] :: False:True → App:Lam:V → App:Lam:V → App:Lam:V → App:Lam:V
and :: False:True → False:True → False:True
False :: False:True
!EQ :: S:0' → S:0' → False:True
mklam :: App:Lam:V → App:Lam:V → App:Lam:V
lamvar :: App:Lam:V → App:Lam:V
lambody :: App:Lam:V → App:Lam:V
isvar :: App:Lam:V → False:True
True :: False:True
islam :: App:Lam:V → False:True
appe2 :: App:Lam:V → App:Lam:V
appe1 :: App:Lam:V → App:Lam:V
lambdaint :: App:Lam:V → App:Lam:V
S :: S:0' → S:0'
0' :: S:0'
red[Let][Let] :: App:Lam:V → App:Lam:V → App:Lam:V → App:Lam:V
hole_App:Lam:V1_0 :: App:Lam:V
hole_S:0'2_0 :: S:0'
hole_False:True3_0 :: False:True
gen_App:Lam:V4_0 :: Nat → App:Lam:V
gen_S:0'5_0 :: Nat → S:0'
(5) OrderProof (LOWER BOUND(ID) transformation)
Heuristically decided to analyse the following defined symbols:
subst,
eqTerm,
red,
!EQThey will be analysed ascendingly in the following order:
eqTerm < subst
subst < red
!EQ < eqTerm
(6) Obligation:
Innermost TRS:
Rules:
subst(
x,
a,
App(
e1,
e2)) →
mkapp(
subst(
x,
a,
e1),
subst(
x,
a,
e2))
subst(
x,
a,
Lam(
var,
exp)) →
subst[True][Ite](
eqTerm(
x,
V(
var)),
x,
a,
Lam(
var,
exp))
red(
App(
e1,
e2)) →
red[Let](
App(
e1,
e2),
red(
e1))
red(
Lam(
int,
term)) →
Lam(
int,
term)
subst(
x,
a,
V(
int)) →
subst[Ite](
eqTerm(
x,
V(
int)),
x,
a,
V(
int))
red(
V(
int)) →
V(
int)
eqTerm(
App(
t11,
t12),
App(
t21,
t22)) →
and(
eqTerm(
t11,
t21),
eqTerm(
t12,
t22))
eqTerm(
App(
t11,
t12),
Lam(
i2,
l2)) →
FalseeqTerm(
App(
t11,
t12),
V(
v2)) →
FalseeqTerm(
Lam(
i1,
l1),
App(
t21,
t22)) →
FalseeqTerm(
Lam(
i1,
l1),
Lam(
i2,
l2)) →
and(
!EQ(
i1,
i2),
eqTerm(
l1,
l2))
eqTerm(
Lam(
i1,
l1),
V(
v2)) →
FalseeqTerm(
V(
v1),
App(
t21,
t22)) →
FalseeqTerm(
V(
v1),
Lam(
i2,
l2)) →
FalseeqTerm(
V(
v1),
V(
v2)) →
!EQ(
v1,
v2)
mklam(
V(
name),
e) →
Lam(
name,
e)
lamvar(
Lam(
var,
exp)) →
V(
var)
lambody(
Lam(
var,
exp)) →
expisvar(
App(
t1,
t2)) →
Falseisvar(
Lam(
int,
term)) →
Falseisvar(
V(
int)) →
Trueislam(
App(
t1,
t2)) →
Falseislam(
Lam(
int,
term)) →
Trueislam(
V(
int)) →
Falseappe2(
App(
e1,
e2)) →
e2appe1(
App(
e1,
e2)) →
e1mkapp(
e1,
e2) →
App(
e1,
e2)
lambdaint(
e) →
red(
e)
and(
False,
False) →
Falseand(
True,
False) →
Falseand(
False,
True) →
Falseand(
True,
True) →
True!EQ(
S(
x),
S(
y)) →
!EQ(
x,
y)
!EQ(
0',
S(
y)) →
False!EQ(
S(
x),
0') →
False!EQ(
0',
0') →
Truered[Let][Let](
e,
Lam(
var,
exp),
a) →
red(
subst(
V(
var),
a,
exp))
subst[True][Ite](
False,
x,
a,
Lam(
var,
exp)) →
mklam(
V(
var),
subst(
x,
a,
exp))
red[Let][Let](
e,
App(
t1,
t2),
e2) →
App(
App(
t1,
t2),
e2)
red[Let][Let](
e,
V(
int),
e2) →
App(
V(
int),
e2)
red[Let](
App(
e1,
e2),
f) →
red[Let][Let](
App(
e1,
e2),
f,
red(
e2))
subst[True][Ite](
True,
x,
a,
e) →
esubst[Ite](
False,
x,
a,
e) →
esubst[Ite](
True,
x,
a,
e) →
aTypes:
subst :: App:Lam:V → App:Lam:V → App:Lam:V → App:Lam:V
App :: App:Lam:V → App:Lam:V → App:Lam:V
mkapp :: App:Lam:V → App:Lam:V → App:Lam:V
Lam :: S:0' → App:Lam:V → App:Lam:V
subst[True][Ite] :: False:True → App:Lam:V → App:Lam:V → App:Lam:V → App:Lam:V
eqTerm :: App:Lam:V → App:Lam:V → False:True
V :: S:0' → App:Lam:V
red :: App:Lam:V → App:Lam:V
red[Let] :: App:Lam:V → App:Lam:V → App:Lam:V
subst[Ite] :: False:True → App:Lam:V → App:Lam:V → App:Lam:V → App:Lam:V
and :: False:True → False:True → False:True
False :: False:True
!EQ :: S:0' → S:0' → False:True
mklam :: App:Lam:V → App:Lam:V → App:Lam:V
lamvar :: App:Lam:V → App:Lam:V
lambody :: App:Lam:V → App:Lam:V
isvar :: App:Lam:V → False:True
True :: False:True
islam :: App:Lam:V → False:True
appe2 :: App:Lam:V → App:Lam:V
appe1 :: App:Lam:V → App:Lam:V
lambdaint :: App:Lam:V → App:Lam:V
S :: S:0' → S:0'
0' :: S:0'
red[Let][Let] :: App:Lam:V → App:Lam:V → App:Lam:V → App:Lam:V
hole_App:Lam:V1_0 :: App:Lam:V
hole_S:0'2_0 :: S:0'
hole_False:True3_0 :: False:True
gen_App:Lam:V4_0 :: Nat → App:Lam:V
gen_S:0'5_0 :: Nat → S:0'
Generator Equations:
gen_App:Lam:V4_0(0) ⇔ V(0')
gen_App:Lam:V4_0(+(x, 1)) ⇔ App(gen_App:Lam:V4_0(x), V(0'))
gen_S:0'5_0(0) ⇔ 0'
gen_S:0'5_0(+(x, 1)) ⇔ S(gen_S:0'5_0(x))
The following defined symbols remain to be analysed:
!EQ, subst, eqTerm, red
They will be analysed ascendingly in the following order:
eqTerm < subst
subst < red
!EQ < eqTerm
(7) RewriteLemmaProof (LOWER BOUND(ID) transformation)
Proved the following rewrite lemma:
!EQ(
gen_S:0'5_0(
n7_0),
gen_S:0'5_0(
+(
1,
n7_0))) →
False, rt ∈ Ω(0)
Induction Base:
!EQ(gen_S:0'5_0(0), gen_S:0'5_0(+(1, 0))) →RΩ(0)
False
Induction Step:
!EQ(gen_S:0'5_0(+(n7_0, 1)), gen_S:0'5_0(+(1, +(n7_0, 1)))) →RΩ(0)
!EQ(gen_S:0'5_0(n7_0), gen_S:0'5_0(+(1, n7_0))) →IH
False
We have rt ∈ Ω(1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n0).
(8) Complex Obligation (BEST)
(9) Obligation:
Innermost TRS:
Rules:
subst(
x,
a,
App(
e1,
e2)) →
mkapp(
subst(
x,
a,
e1),
subst(
x,
a,
e2))
subst(
x,
a,
Lam(
var,
exp)) →
subst[True][Ite](
eqTerm(
x,
V(
var)),
x,
a,
Lam(
var,
exp))
red(
App(
e1,
e2)) →
red[Let](
App(
e1,
e2),
red(
e1))
red(
Lam(
int,
term)) →
Lam(
int,
term)
subst(
x,
a,
V(
int)) →
subst[Ite](
eqTerm(
x,
V(
int)),
x,
a,
V(
int))
red(
V(
int)) →
V(
int)
eqTerm(
App(
t11,
t12),
App(
t21,
t22)) →
and(
eqTerm(
t11,
t21),
eqTerm(
t12,
t22))
eqTerm(
App(
t11,
t12),
Lam(
i2,
l2)) →
FalseeqTerm(
App(
t11,
t12),
V(
v2)) →
FalseeqTerm(
Lam(
i1,
l1),
App(
t21,
t22)) →
FalseeqTerm(
Lam(
i1,
l1),
Lam(
i2,
l2)) →
and(
!EQ(
i1,
i2),
eqTerm(
l1,
l2))
eqTerm(
Lam(
i1,
l1),
V(
v2)) →
FalseeqTerm(
V(
v1),
App(
t21,
t22)) →
FalseeqTerm(
V(
v1),
Lam(
i2,
l2)) →
FalseeqTerm(
V(
v1),
V(
v2)) →
!EQ(
v1,
v2)
mklam(
V(
name),
e) →
Lam(
name,
e)
lamvar(
Lam(
var,
exp)) →
V(
var)
lambody(
Lam(
var,
exp)) →
expisvar(
App(
t1,
t2)) →
Falseisvar(
Lam(
int,
term)) →
Falseisvar(
V(
int)) →
Trueislam(
App(
t1,
t2)) →
Falseislam(
Lam(
int,
term)) →
Trueislam(
V(
int)) →
Falseappe2(
App(
e1,
e2)) →
e2appe1(
App(
e1,
e2)) →
e1mkapp(
e1,
e2) →
App(
e1,
e2)
lambdaint(
e) →
red(
e)
and(
False,
False) →
Falseand(
True,
False) →
Falseand(
False,
True) →
Falseand(
True,
True) →
True!EQ(
S(
x),
S(
y)) →
!EQ(
x,
y)
!EQ(
0',
S(
y)) →
False!EQ(
S(
x),
0') →
False!EQ(
0',
0') →
Truered[Let][Let](
e,
Lam(
var,
exp),
a) →
red(
subst(
V(
var),
a,
exp))
subst[True][Ite](
False,
x,
a,
Lam(
var,
exp)) →
mklam(
V(
var),
subst(
x,
a,
exp))
red[Let][Let](
e,
App(
t1,
t2),
e2) →
App(
App(
t1,
t2),
e2)
red[Let][Let](
e,
V(
int),
e2) →
App(
V(
int),
e2)
red[Let](
App(
e1,
e2),
f) →
red[Let][Let](
App(
e1,
e2),
f,
red(
e2))
subst[True][Ite](
True,
x,
a,
e) →
esubst[Ite](
False,
x,
a,
e) →
esubst[Ite](
True,
x,
a,
e) →
aTypes:
subst :: App:Lam:V → App:Lam:V → App:Lam:V → App:Lam:V
App :: App:Lam:V → App:Lam:V → App:Lam:V
mkapp :: App:Lam:V → App:Lam:V → App:Lam:V
Lam :: S:0' → App:Lam:V → App:Lam:V
subst[True][Ite] :: False:True → App:Lam:V → App:Lam:V → App:Lam:V → App:Lam:V
eqTerm :: App:Lam:V → App:Lam:V → False:True
V :: S:0' → App:Lam:V
red :: App:Lam:V → App:Lam:V
red[Let] :: App:Lam:V → App:Lam:V → App:Lam:V
subst[Ite] :: False:True → App:Lam:V → App:Lam:V → App:Lam:V → App:Lam:V
and :: False:True → False:True → False:True
False :: False:True
!EQ :: S:0' → S:0' → False:True
mklam :: App:Lam:V → App:Lam:V → App:Lam:V
lamvar :: App:Lam:V → App:Lam:V
lambody :: App:Lam:V → App:Lam:V
isvar :: App:Lam:V → False:True
True :: False:True
islam :: App:Lam:V → False:True
appe2 :: App:Lam:V → App:Lam:V
appe1 :: App:Lam:V → App:Lam:V
lambdaint :: App:Lam:V → App:Lam:V
S :: S:0' → S:0'
0' :: S:0'
red[Let][Let] :: App:Lam:V → App:Lam:V → App:Lam:V → App:Lam:V
hole_App:Lam:V1_0 :: App:Lam:V
hole_S:0'2_0 :: S:0'
hole_False:True3_0 :: False:True
gen_App:Lam:V4_0 :: Nat → App:Lam:V
gen_S:0'5_0 :: Nat → S:0'
Lemmas:
!EQ(gen_S:0'5_0(n7_0), gen_S:0'5_0(+(1, n7_0))) → False, rt ∈ Ω(0)
Generator Equations:
gen_App:Lam:V4_0(0) ⇔ V(0')
gen_App:Lam:V4_0(+(x, 1)) ⇔ App(gen_App:Lam:V4_0(x), V(0'))
gen_S:0'5_0(0) ⇔ 0'
gen_S:0'5_0(+(x, 1)) ⇔ S(gen_S:0'5_0(x))
The following defined symbols remain to be analysed:
eqTerm, subst, red
They will be analysed ascendingly in the following order:
eqTerm < subst
subst < red
(10) RewriteLemmaProof (LOWER BOUND(ID) transformation)
Proved the following rewrite lemma:
eqTerm(
gen_App:Lam:V4_0(
+(
1,
n510_0)),
gen_App:Lam:V4_0(
n510_0)) →
False, rt ∈ Ω(1 + n510
0)
Induction Base:
eqTerm(gen_App:Lam:V4_0(+(1, 0)), gen_App:Lam:V4_0(0)) →RΩ(1)
False
Induction Step:
eqTerm(gen_App:Lam:V4_0(+(1, +(n510_0, 1))), gen_App:Lam:V4_0(+(n510_0, 1))) →RΩ(1)
and(eqTerm(gen_App:Lam:V4_0(+(1, n510_0)), gen_App:Lam:V4_0(n510_0)), eqTerm(V(0'), V(0'))) →IH
and(False, eqTerm(V(0'), V(0'))) →RΩ(1)
and(False, !EQ(0', 0')) →RΩ(0)
and(False, True) →RΩ(0)
False
We have rt ∈ Ω(n1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
(11) Complex Obligation (BEST)
(12) Obligation:
Innermost TRS:
Rules:
subst(
x,
a,
App(
e1,
e2)) →
mkapp(
subst(
x,
a,
e1),
subst(
x,
a,
e2))
subst(
x,
a,
Lam(
var,
exp)) →
subst[True][Ite](
eqTerm(
x,
V(
var)),
x,
a,
Lam(
var,
exp))
red(
App(
e1,
e2)) →
red[Let](
App(
e1,
e2),
red(
e1))
red(
Lam(
int,
term)) →
Lam(
int,
term)
subst(
x,
a,
V(
int)) →
subst[Ite](
eqTerm(
x,
V(
int)),
x,
a,
V(
int))
red(
V(
int)) →
V(
int)
eqTerm(
App(
t11,
t12),
App(
t21,
t22)) →
and(
eqTerm(
t11,
t21),
eqTerm(
t12,
t22))
eqTerm(
App(
t11,
t12),
Lam(
i2,
l2)) →
FalseeqTerm(
App(
t11,
t12),
V(
v2)) →
FalseeqTerm(
Lam(
i1,
l1),
App(
t21,
t22)) →
FalseeqTerm(
Lam(
i1,
l1),
Lam(
i2,
l2)) →
and(
!EQ(
i1,
i2),
eqTerm(
l1,
l2))
eqTerm(
Lam(
i1,
l1),
V(
v2)) →
FalseeqTerm(
V(
v1),
App(
t21,
t22)) →
FalseeqTerm(
V(
v1),
Lam(
i2,
l2)) →
FalseeqTerm(
V(
v1),
V(
v2)) →
!EQ(
v1,
v2)
mklam(
V(
name),
e) →
Lam(
name,
e)
lamvar(
Lam(
var,
exp)) →
V(
var)
lambody(
Lam(
var,
exp)) →
expisvar(
App(
t1,
t2)) →
Falseisvar(
Lam(
int,
term)) →
Falseisvar(
V(
int)) →
Trueislam(
App(
t1,
t2)) →
Falseislam(
Lam(
int,
term)) →
Trueislam(
V(
int)) →
Falseappe2(
App(
e1,
e2)) →
e2appe1(
App(
e1,
e2)) →
e1mkapp(
e1,
e2) →
App(
e1,
e2)
lambdaint(
e) →
red(
e)
and(
False,
False) →
Falseand(
True,
False) →
Falseand(
False,
True) →
Falseand(
True,
True) →
True!EQ(
S(
x),
S(
y)) →
!EQ(
x,
y)
!EQ(
0',
S(
y)) →
False!EQ(
S(
x),
0') →
False!EQ(
0',
0') →
Truered[Let][Let](
e,
Lam(
var,
exp),
a) →
red(
subst(
V(
var),
a,
exp))
subst[True][Ite](
False,
x,
a,
Lam(
var,
exp)) →
mklam(
V(
var),
subst(
x,
a,
exp))
red[Let][Let](
e,
App(
t1,
t2),
e2) →
App(
App(
t1,
t2),
e2)
red[Let][Let](
e,
V(
int),
e2) →
App(
V(
int),
e2)
red[Let](
App(
e1,
e2),
f) →
red[Let][Let](
App(
e1,
e2),
f,
red(
e2))
subst[True][Ite](
True,
x,
a,
e) →
esubst[Ite](
False,
x,
a,
e) →
esubst[Ite](
True,
x,
a,
e) →
aTypes:
subst :: App:Lam:V → App:Lam:V → App:Lam:V → App:Lam:V
App :: App:Lam:V → App:Lam:V → App:Lam:V
mkapp :: App:Lam:V → App:Lam:V → App:Lam:V
Lam :: S:0' → App:Lam:V → App:Lam:V
subst[True][Ite] :: False:True → App:Lam:V → App:Lam:V → App:Lam:V → App:Lam:V
eqTerm :: App:Lam:V → App:Lam:V → False:True
V :: S:0' → App:Lam:V
red :: App:Lam:V → App:Lam:V
red[Let] :: App:Lam:V → App:Lam:V → App:Lam:V
subst[Ite] :: False:True → App:Lam:V → App:Lam:V → App:Lam:V → App:Lam:V
and :: False:True → False:True → False:True
False :: False:True
!EQ :: S:0' → S:0' → False:True
mklam :: App:Lam:V → App:Lam:V → App:Lam:V
lamvar :: App:Lam:V → App:Lam:V
lambody :: App:Lam:V → App:Lam:V
isvar :: App:Lam:V → False:True
True :: False:True
islam :: App:Lam:V → False:True
appe2 :: App:Lam:V → App:Lam:V
appe1 :: App:Lam:V → App:Lam:V
lambdaint :: App:Lam:V → App:Lam:V
S :: S:0' → S:0'
0' :: S:0'
red[Let][Let] :: App:Lam:V → App:Lam:V → App:Lam:V → App:Lam:V
hole_App:Lam:V1_0 :: App:Lam:V
hole_S:0'2_0 :: S:0'
hole_False:True3_0 :: False:True
gen_App:Lam:V4_0 :: Nat → App:Lam:V
gen_S:0'5_0 :: Nat → S:0'
Lemmas:
!EQ(gen_S:0'5_0(n7_0), gen_S:0'5_0(+(1, n7_0))) → False, rt ∈ Ω(0)
eqTerm(gen_App:Lam:V4_0(+(1, n510_0)), gen_App:Lam:V4_0(n510_0)) → False, rt ∈ Ω(1 + n5100)
Generator Equations:
gen_App:Lam:V4_0(0) ⇔ V(0')
gen_App:Lam:V4_0(+(x, 1)) ⇔ App(gen_App:Lam:V4_0(x), V(0'))
gen_S:0'5_0(0) ⇔ 0'
gen_S:0'5_0(+(x, 1)) ⇔ S(gen_S:0'5_0(x))
The following defined symbols remain to be analysed:
subst, red
They will be analysed ascendingly in the following order:
subst < red
(13) RewriteLemmaProof (LOWER BOUND(ID) transformation)
Proved the following rewrite lemma:
subst(
gen_App:Lam:V4_0(
1),
gen_App:Lam:V4_0(
b),
gen_App:Lam:V4_0(
n369658_0)) →
gen_App:Lam:V4_0(
n369658_0), rt ∈ Ω(1 + n369658
0)
Induction Base:
subst(gen_App:Lam:V4_0(1), gen_App:Lam:V4_0(b), gen_App:Lam:V4_0(0)) →RΩ(1)
subst[Ite](eqTerm(gen_App:Lam:V4_0(1), V(0')), gen_App:Lam:V4_0(1), gen_App:Lam:V4_0(b), V(0')) →LΩ(1)
subst[Ite](False, gen_App:Lam:V4_0(1), gen_App:Lam:V4_0(b), V(0')) →RΩ(0)
V(0')
Induction Step:
subst(gen_App:Lam:V4_0(1), gen_App:Lam:V4_0(b), gen_App:Lam:V4_0(+(n369658_0, 1))) →RΩ(1)
mkapp(subst(gen_App:Lam:V4_0(1), gen_App:Lam:V4_0(b), gen_App:Lam:V4_0(n369658_0)), subst(gen_App:Lam:V4_0(1), gen_App:Lam:V4_0(b), V(0'))) →IH
mkapp(gen_App:Lam:V4_0(c369659_0), subst(gen_App:Lam:V4_0(1), gen_App:Lam:V4_0(b), V(0'))) →RΩ(1)
mkapp(gen_App:Lam:V4_0(n369658_0), subst[Ite](eqTerm(gen_App:Lam:V4_0(1), V(0')), gen_App:Lam:V4_0(1), gen_App:Lam:V4_0(b), V(0'))) →LΩ(1)
mkapp(gen_App:Lam:V4_0(n369658_0), subst[Ite](False, gen_App:Lam:V4_0(1), gen_App:Lam:V4_0(b), V(0'))) →RΩ(0)
mkapp(gen_App:Lam:V4_0(n369658_0), V(0')) →RΩ(1)
App(gen_App:Lam:V4_0(n369658_0), V(0'))
We have rt ∈ Ω(n1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
(14) Complex Obligation (BEST)
(15) Obligation:
Innermost TRS:
Rules:
subst(
x,
a,
App(
e1,
e2)) →
mkapp(
subst(
x,
a,
e1),
subst(
x,
a,
e2))
subst(
x,
a,
Lam(
var,
exp)) →
subst[True][Ite](
eqTerm(
x,
V(
var)),
x,
a,
Lam(
var,
exp))
red(
App(
e1,
e2)) →
red[Let](
App(
e1,
e2),
red(
e1))
red(
Lam(
int,
term)) →
Lam(
int,
term)
subst(
x,
a,
V(
int)) →
subst[Ite](
eqTerm(
x,
V(
int)),
x,
a,
V(
int))
red(
V(
int)) →
V(
int)
eqTerm(
App(
t11,
t12),
App(
t21,
t22)) →
and(
eqTerm(
t11,
t21),
eqTerm(
t12,
t22))
eqTerm(
App(
t11,
t12),
Lam(
i2,
l2)) →
FalseeqTerm(
App(
t11,
t12),
V(
v2)) →
FalseeqTerm(
Lam(
i1,
l1),
App(
t21,
t22)) →
FalseeqTerm(
Lam(
i1,
l1),
Lam(
i2,
l2)) →
and(
!EQ(
i1,
i2),
eqTerm(
l1,
l2))
eqTerm(
Lam(
i1,
l1),
V(
v2)) →
FalseeqTerm(
V(
v1),
App(
t21,
t22)) →
FalseeqTerm(
V(
v1),
Lam(
i2,
l2)) →
FalseeqTerm(
V(
v1),
V(
v2)) →
!EQ(
v1,
v2)
mklam(
V(
name),
e) →
Lam(
name,
e)
lamvar(
Lam(
var,
exp)) →
V(
var)
lambody(
Lam(
var,
exp)) →
expisvar(
App(
t1,
t2)) →
Falseisvar(
Lam(
int,
term)) →
Falseisvar(
V(
int)) →
Trueislam(
App(
t1,
t2)) →
Falseislam(
Lam(
int,
term)) →
Trueislam(
V(
int)) →
Falseappe2(
App(
e1,
e2)) →
e2appe1(
App(
e1,
e2)) →
e1mkapp(
e1,
e2) →
App(
e1,
e2)
lambdaint(
e) →
red(
e)
and(
False,
False) →
Falseand(
True,
False) →
Falseand(
False,
True) →
Falseand(
True,
True) →
True!EQ(
S(
x),
S(
y)) →
!EQ(
x,
y)
!EQ(
0',
S(
y)) →
False!EQ(
S(
x),
0') →
False!EQ(
0',
0') →
Truered[Let][Let](
e,
Lam(
var,
exp),
a) →
red(
subst(
V(
var),
a,
exp))
subst[True][Ite](
False,
x,
a,
Lam(
var,
exp)) →
mklam(
V(
var),
subst(
x,
a,
exp))
red[Let][Let](
e,
App(
t1,
t2),
e2) →
App(
App(
t1,
t2),
e2)
red[Let][Let](
e,
V(
int),
e2) →
App(
V(
int),
e2)
red[Let](
App(
e1,
e2),
f) →
red[Let][Let](
App(
e1,
e2),
f,
red(
e2))
subst[True][Ite](
True,
x,
a,
e) →
esubst[Ite](
False,
x,
a,
e) →
esubst[Ite](
True,
x,
a,
e) →
aTypes:
subst :: App:Lam:V → App:Lam:V → App:Lam:V → App:Lam:V
App :: App:Lam:V → App:Lam:V → App:Lam:V
mkapp :: App:Lam:V → App:Lam:V → App:Lam:V
Lam :: S:0' → App:Lam:V → App:Lam:V
subst[True][Ite] :: False:True → App:Lam:V → App:Lam:V → App:Lam:V → App:Lam:V
eqTerm :: App:Lam:V → App:Lam:V → False:True
V :: S:0' → App:Lam:V
red :: App:Lam:V → App:Lam:V
red[Let] :: App:Lam:V → App:Lam:V → App:Lam:V
subst[Ite] :: False:True → App:Lam:V → App:Lam:V → App:Lam:V → App:Lam:V
and :: False:True → False:True → False:True
False :: False:True
!EQ :: S:0' → S:0' → False:True
mklam :: App:Lam:V → App:Lam:V → App:Lam:V
lamvar :: App:Lam:V → App:Lam:V
lambody :: App:Lam:V → App:Lam:V
isvar :: App:Lam:V → False:True
True :: False:True
islam :: App:Lam:V → False:True
appe2 :: App:Lam:V → App:Lam:V
appe1 :: App:Lam:V → App:Lam:V
lambdaint :: App:Lam:V → App:Lam:V
S :: S:0' → S:0'
0' :: S:0'
red[Let][Let] :: App:Lam:V → App:Lam:V → App:Lam:V → App:Lam:V
hole_App:Lam:V1_0 :: App:Lam:V
hole_S:0'2_0 :: S:0'
hole_False:True3_0 :: False:True
gen_App:Lam:V4_0 :: Nat → App:Lam:V
gen_S:0'5_0 :: Nat → S:0'
Lemmas:
!EQ(gen_S:0'5_0(n7_0), gen_S:0'5_0(+(1, n7_0))) → False, rt ∈ Ω(0)
eqTerm(gen_App:Lam:V4_0(+(1, n510_0)), gen_App:Lam:V4_0(n510_0)) → False, rt ∈ Ω(1 + n5100)
subst(gen_App:Lam:V4_0(1), gen_App:Lam:V4_0(b), gen_App:Lam:V4_0(n369658_0)) → gen_App:Lam:V4_0(n369658_0), rt ∈ Ω(1 + n3696580)
Generator Equations:
gen_App:Lam:V4_0(0) ⇔ V(0')
gen_App:Lam:V4_0(+(x, 1)) ⇔ App(gen_App:Lam:V4_0(x), V(0'))
gen_S:0'5_0(0) ⇔ 0'
gen_S:0'5_0(+(x, 1)) ⇔ S(gen_S:0'5_0(x))
The following defined symbols remain to be analysed:
red
(16) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol red.
(17) Obligation:
Innermost TRS:
Rules:
subst(
x,
a,
App(
e1,
e2)) →
mkapp(
subst(
x,
a,
e1),
subst(
x,
a,
e2))
subst(
x,
a,
Lam(
var,
exp)) →
subst[True][Ite](
eqTerm(
x,
V(
var)),
x,
a,
Lam(
var,
exp))
red(
App(
e1,
e2)) →
red[Let](
App(
e1,
e2),
red(
e1))
red(
Lam(
int,
term)) →
Lam(
int,
term)
subst(
x,
a,
V(
int)) →
subst[Ite](
eqTerm(
x,
V(
int)),
x,
a,
V(
int))
red(
V(
int)) →
V(
int)
eqTerm(
App(
t11,
t12),
App(
t21,
t22)) →
and(
eqTerm(
t11,
t21),
eqTerm(
t12,
t22))
eqTerm(
App(
t11,
t12),
Lam(
i2,
l2)) →
FalseeqTerm(
App(
t11,
t12),
V(
v2)) →
FalseeqTerm(
Lam(
i1,
l1),
App(
t21,
t22)) →
FalseeqTerm(
Lam(
i1,
l1),
Lam(
i2,
l2)) →
and(
!EQ(
i1,
i2),
eqTerm(
l1,
l2))
eqTerm(
Lam(
i1,
l1),
V(
v2)) →
FalseeqTerm(
V(
v1),
App(
t21,
t22)) →
FalseeqTerm(
V(
v1),
Lam(
i2,
l2)) →
FalseeqTerm(
V(
v1),
V(
v2)) →
!EQ(
v1,
v2)
mklam(
V(
name),
e) →
Lam(
name,
e)
lamvar(
Lam(
var,
exp)) →
V(
var)
lambody(
Lam(
var,
exp)) →
expisvar(
App(
t1,
t2)) →
Falseisvar(
Lam(
int,
term)) →
Falseisvar(
V(
int)) →
Trueislam(
App(
t1,
t2)) →
Falseislam(
Lam(
int,
term)) →
Trueislam(
V(
int)) →
Falseappe2(
App(
e1,
e2)) →
e2appe1(
App(
e1,
e2)) →
e1mkapp(
e1,
e2) →
App(
e1,
e2)
lambdaint(
e) →
red(
e)
and(
False,
False) →
Falseand(
True,
False) →
Falseand(
False,
True) →
Falseand(
True,
True) →
True!EQ(
S(
x),
S(
y)) →
!EQ(
x,
y)
!EQ(
0',
S(
y)) →
False!EQ(
S(
x),
0') →
False!EQ(
0',
0') →
Truered[Let][Let](
e,
Lam(
var,
exp),
a) →
red(
subst(
V(
var),
a,
exp))
subst[True][Ite](
False,
x,
a,
Lam(
var,
exp)) →
mklam(
V(
var),
subst(
x,
a,
exp))
red[Let][Let](
e,
App(
t1,
t2),
e2) →
App(
App(
t1,
t2),
e2)
red[Let][Let](
e,
V(
int),
e2) →
App(
V(
int),
e2)
red[Let](
App(
e1,
e2),
f) →
red[Let][Let](
App(
e1,
e2),
f,
red(
e2))
subst[True][Ite](
True,
x,
a,
e) →
esubst[Ite](
False,
x,
a,
e) →
esubst[Ite](
True,
x,
a,
e) →
aTypes:
subst :: App:Lam:V → App:Lam:V → App:Lam:V → App:Lam:V
App :: App:Lam:V → App:Lam:V → App:Lam:V
mkapp :: App:Lam:V → App:Lam:V → App:Lam:V
Lam :: S:0' → App:Lam:V → App:Lam:V
subst[True][Ite] :: False:True → App:Lam:V → App:Lam:V → App:Lam:V → App:Lam:V
eqTerm :: App:Lam:V → App:Lam:V → False:True
V :: S:0' → App:Lam:V
red :: App:Lam:V → App:Lam:V
red[Let] :: App:Lam:V → App:Lam:V → App:Lam:V
subst[Ite] :: False:True → App:Lam:V → App:Lam:V → App:Lam:V → App:Lam:V
and :: False:True → False:True → False:True
False :: False:True
!EQ :: S:0' → S:0' → False:True
mklam :: App:Lam:V → App:Lam:V → App:Lam:V
lamvar :: App:Lam:V → App:Lam:V
lambody :: App:Lam:V → App:Lam:V
isvar :: App:Lam:V → False:True
True :: False:True
islam :: App:Lam:V → False:True
appe2 :: App:Lam:V → App:Lam:V
appe1 :: App:Lam:V → App:Lam:V
lambdaint :: App:Lam:V → App:Lam:V
S :: S:0' → S:0'
0' :: S:0'
red[Let][Let] :: App:Lam:V → App:Lam:V → App:Lam:V → App:Lam:V
hole_App:Lam:V1_0 :: App:Lam:V
hole_S:0'2_0 :: S:0'
hole_False:True3_0 :: False:True
gen_App:Lam:V4_0 :: Nat → App:Lam:V
gen_S:0'5_0 :: Nat → S:0'
Lemmas:
!EQ(gen_S:0'5_0(n7_0), gen_S:0'5_0(+(1, n7_0))) → False, rt ∈ Ω(0)
eqTerm(gen_App:Lam:V4_0(+(1, n510_0)), gen_App:Lam:V4_0(n510_0)) → False, rt ∈ Ω(1 + n5100)
subst(gen_App:Lam:V4_0(1), gen_App:Lam:V4_0(b), gen_App:Lam:V4_0(n369658_0)) → gen_App:Lam:V4_0(n369658_0), rt ∈ Ω(1 + n3696580)
Generator Equations:
gen_App:Lam:V4_0(0) ⇔ V(0')
gen_App:Lam:V4_0(+(x, 1)) ⇔ App(gen_App:Lam:V4_0(x), V(0'))
gen_S:0'5_0(0) ⇔ 0'
gen_S:0'5_0(+(x, 1)) ⇔ S(gen_S:0'5_0(x))
No more defined symbols left to analyse.
(18) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(n1) was proven with the following lemma:
eqTerm(gen_App:Lam:V4_0(+(1, n510_0)), gen_App:Lam:V4_0(n510_0)) → False, rt ∈ Ω(1 + n5100)
(19) BOUNDS(n^1, INF)
(20) Obligation:
Innermost TRS:
Rules:
subst(
x,
a,
App(
e1,
e2)) →
mkapp(
subst(
x,
a,
e1),
subst(
x,
a,
e2))
subst(
x,
a,
Lam(
var,
exp)) →
subst[True][Ite](
eqTerm(
x,
V(
var)),
x,
a,
Lam(
var,
exp))
red(
App(
e1,
e2)) →
red[Let](
App(
e1,
e2),
red(
e1))
red(
Lam(
int,
term)) →
Lam(
int,
term)
subst(
x,
a,
V(
int)) →
subst[Ite](
eqTerm(
x,
V(
int)),
x,
a,
V(
int))
red(
V(
int)) →
V(
int)
eqTerm(
App(
t11,
t12),
App(
t21,
t22)) →
and(
eqTerm(
t11,
t21),
eqTerm(
t12,
t22))
eqTerm(
App(
t11,
t12),
Lam(
i2,
l2)) →
FalseeqTerm(
App(
t11,
t12),
V(
v2)) →
FalseeqTerm(
Lam(
i1,
l1),
App(
t21,
t22)) →
FalseeqTerm(
Lam(
i1,
l1),
Lam(
i2,
l2)) →
and(
!EQ(
i1,
i2),
eqTerm(
l1,
l2))
eqTerm(
Lam(
i1,
l1),
V(
v2)) →
FalseeqTerm(
V(
v1),
App(
t21,
t22)) →
FalseeqTerm(
V(
v1),
Lam(
i2,
l2)) →
FalseeqTerm(
V(
v1),
V(
v2)) →
!EQ(
v1,
v2)
mklam(
V(
name),
e) →
Lam(
name,
e)
lamvar(
Lam(
var,
exp)) →
V(
var)
lambody(
Lam(
var,
exp)) →
expisvar(
App(
t1,
t2)) →
Falseisvar(
Lam(
int,
term)) →
Falseisvar(
V(
int)) →
Trueislam(
App(
t1,
t2)) →
Falseislam(
Lam(
int,
term)) →
Trueislam(
V(
int)) →
Falseappe2(
App(
e1,
e2)) →
e2appe1(
App(
e1,
e2)) →
e1mkapp(
e1,
e2) →
App(
e1,
e2)
lambdaint(
e) →
red(
e)
and(
False,
False) →
Falseand(
True,
False) →
Falseand(
False,
True) →
Falseand(
True,
True) →
True!EQ(
S(
x),
S(
y)) →
!EQ(
x,
y)
!EQ(
0',
S(
y)) →
False!EQ(
S(
x),
0') →
False!EQ(
0',
0') →
Truered[Let][Let](
e,
Lam(
var,
exp),
a) →
red(
subst(
V(
var),
a,
exp))
subst[True][Ite](
False,
x,
a,
Lam(
var,
exp)) →
mklam(
V(
var),
subst(
x,
a,
exp))
red[Let][Let](
e,
App(
t1,
t2),
e2) →
App(
App(
t1,
t2),
e2)
red[Let][Let](
e,
V(
int),
e2) →
App(
V(
int),
e2)
red[Let](
App(
e1,
e2),
f) →
red[Let][Let](
App(
e1,
e2),
f,
red(
e2))
subst[True][Ite](
True,
x,
a,
e) →
esubst[Ite](
False,
x,
a,
e) →
esubst[Ite](
True,
x,
a,
e) →
aTypes:
subst :: App:Lam:V → App:Lam:V → App:Lam:V → App:Lam:V
App :: App:Lam:V → App:Lam:V → App:Lam:V
mkapp :: App:Lam:V → App:Lam:V → App:Lam:V
Lam :: S:0' → App:Lam:V → App:Lam:V
subst[True][Ite] :: False:True → App:Lam:V → App:Lam:V → App:Lam:V → App:Lam:V
eqTerm :: App:Lam:V → App:Lam:V → False:True
V :: S:0' → App:Lam:V
red :: App:Lam:V → App:Lam:V
red[Let] :: App:Lam:V → App:Lam:V → App:Lam:V
subst[Ite] :: False:True → App:Lam:V → App:Lam:V → App:Lam:V → App:Lam:V
and :: False:True → False:True → False:True
False :: False:True
!EQ :: S:0' → S:0' → False:True
mklam :: App:Lam:V → App:Lam:V → App:Lam:V
lamvar :: App:Lam:V → App:Lam:V
lambody :: App:Lam:V → App:Lam:V
isvar :: App:Lam:V → False:True
True :: False:True
islam :: App:Lam:V → False:True
appe2 :: App:Lam:V → App:Lam:V
appe1 :: App:Lam:V → App:Lam:V
lambdaint :: App:Lam:V → App:Lam:V
S :: S:0' → S:0'
0' :: S:0'
red[Let][Let] :: App:Lam:V → App:Lam:V → App:Lam:V → App:Lam:V
hole_App:Lam:V1_0 :: App:Lam:V
hole_S:0'2_0 :: S:0'
hole_False:True3_0 :: False:True
gen_App:Lam:V4_0 :: Nat → App:Lam:V
gen_S:0'5_0 :: Nat → S:0'
Lemmas:
!EQ(gen_S:0'5_0(n7_0), gen_S:0'5_0(+(1, n7_0))) → False, rt ∈ Ω(0)
eqTerm(gen_App:Lam:V4_0(+(1, n510_0)), gen_App:Lam:V4_0(n510_0)) → False, rt ∈ Ω(1 + n5100)
subst(gen_App:Lam:V4_0(1), gen_App:Lam:V4_0(b), gen_App:Lam:V4_0(n369658_0)) → gen_App:Lam:V4_0(n369658_0), rt ∈ Ω(1 + n3696580)
Generator Equations:
gen_App:Lam:V4_0(0) ⇔ V(0')
gen_App:Lam:V4_0(+(x, 1)) ⇔ App(gen_App:Lam:V4_0(x), V(0'))
gen_S:0'5_0(0) ⇔ 0'
gen_S:0'5_0(+(x, 1)) ⇔ S(gen_S:0'5_0(x))
No more defined symbols left to analyse.
(21) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(n1) was proven with the following lemma:
eqTerm(gen_App:Lam:V4_0(+(1, n510_0)), gen_App:Lam:V4_0(n510_0)) → False, rt ∈ Ω(1 + n5100)
(22) BOUNDS(n^1, INF)
(23) Obligation:
Innermost TRS:
Rules:
subst(
x,
a,
App(
e1,
e2)) →
mkapp(
subst(
x,
a,
e1),
subst(
x,
a,
e2))
subst(
x,
a,
Lam(
var,
exp)) →
subst[True][Ite](
eqTerm(
x,
V(
var)),
x,
a,
Lam(
var,
exp))
red(
App(
e1,
e2)) →
red[Let](
App(
e1,
e2),
red(
e1))
red(
Lam(
int,
term)) →
Lam(
int,
term)
subst(
x,
a,
V(
int)) →
subst[Ite](
eqTerm(
x,
V(
int)),
x,
a,
V(
int))
red(
V(
int)) →
V(
int)
eqTerm(
App(
t11,
t12),
App(
t21,
t22)) →
and(
eqTerm(
t11,
t21),
eqTerm(
t12,
t22))
eqTerm(
App(
t11,
t12),
Lam(
i2,
l2)) →
FalseeqTerm(
App(
t11,
t12),
V(
v2)) →
FalseeqTerm(
Lam(
i1,
l1),
App(
t21,
t22)) →
FalseeqTerm(
Lam(
i1,
l1),
Lam(
i2,
l2)) →
and(
!EQ(
i1,
i2),
eqTerm(
l1,
l2))
eqTerm(
Lam(
i1,
l1),
V(
v2)) →
FalseeqTerm(
V(
v1),
App(
t21,
t22)) →
FalseeqTerm(
V(
v1),
Lam(
i2,
l2)) →
FalseeqTerm(
V(
v1),
V(
v2)) →
!EQ(
v1,
v2)
mklam(
V(
name),
e) →
Lam(
name,
e)
lamvar(
Lam(
var,
exp)) →
V(
var)
lambody(
Lam(
var,
exp)) →
expisvar(
App(
t1,
t2)) →
Falseisvar(
Lam(
int,
term)) →
Falseisvar(
V(
int)) →
Trueislam(
App(
t1,
t2)) →
Falseislam(
Lam(
int,
term)) →
Trueislam(
V(
int)) →
Falseappe2(
App(
e1,
e2)) →
e2appe1(
App(
e1,
e2)) →
e1mkapp(
e1,
e2) →
App(
e1,
e2)
lambdaint(
e) →
red(
e)
and(
False,
False) →
Falseand(
True,
False) →
Falseand(
False,
True) →
Falseand(
True,
True) →
True!EQ(
S(
x),
S(
y)) →
!EQ(
x,
y)
!EQ(
0',
S(
y)) →
False!EQ(
S(
x),
0') →
False!EQ(
0',
0') →
Truered[Let][Let](
e,
Lam(
var,
exp),
a) →
red(
subst(
V(
var),
a,
exp))
subst[True][Ite](
False,
x,
a,
Lam(
var,
exp)) →
mklam(
V(
var),
subst(
x,
a,
exp))
red[Let][Let](
e,
App(
t1,
t2),
e2) →
App(
App(
t1,
t2),
e2)
red[Let][Let](
e,
V(
int),
e2) →
App(
V(
int),
e2)
red[Let](
App(
e1,
e2),
f) →
red[Let][Let](
App(
e1,
e2),
f,
red(
e2))
subst[True][Ite](
True,
x,
a,
e) →
esubst[Ite](
False,
x,
a,
e) →
esubst[Ite](
True,
x,
a,
e) →
aTypes:
subst :: App:Lam:V → App:Lam:V → App:Lam:V → App:Lam:V
App :: App:Lam:V → App:Lam:V → App:Lam:V
mkapp :: App:Lam:V → App:Lam:V → App:Lam:V
Lam :: S:0' → App:Lam:V → App:Lam:V
subst[True][Ite] :: False:True → App:Lam:V → App:Lam:V → App:Lam:V → App:Lam:V
eqTerm :: App:Lam:V → App:Lam:V → False:True
V :: S:0' → App:Lam:V
red :: App:Lam:V → App:Lam:V
red[Let] :: App:Lam:V → App:Lam:V → App:Lam:V
subst[Ite] :: False:True → App:Lam:V → App:Lam:V → App:Lam:V → App:Lam:V
and :: False:True → False:True → False:True
False :: False:True
!EQ :: S:0' → S:0' → False:True
mklam :: App:Lam:V → App:Lam:V → App:Lam:V
lamvar :: App:Lam:V → App:Lam:V
lambody :: App:Lam:V → App:Lam:V
isvar :: App:Lam:V → False:True
True :: False:True
islam :: App:Lam:V → False:True
appe2 :: App:Lam:V → App:Lam:V
appe1 :: App:Lam:V → App:Lam:V
lambdaint :: App:Lam:V → App:Lam:V
S :: S:0' → S:0'
0' :: S:0'
red[Let][Let] :: App:Lam:V → App:Lam:V → App:Lam:V → App:Lam:V
hole_App:Lam:V1_0 :: App:Lam:V
hole_S:0'2_0 :: S:0'
hole_False:True3_0 :: False:True
gen_App:Lam:V4_0 :: Nat → App:Lam:V
gen_S:0'5_0 :: Nat → S:0'
Lemmas:
!EQ(gen_S:0'5_0(n7_0), gen_S:0'5_0(+(1, n7_0))) → False, rt ∈ Ω(0)
eqTerm(gen_App:Lam:V4_0(+(1, n510_0)), gen_App:Lam:V4_0(n510_0)) → False, rt ∈ Ω(1 + n5100)
Generator Equations:
gen_App:Lam:V4_0(0) ⇔ V(0')
gen_App:Lam:V4_0(+(x, 1)) ⇔ App(gen_App:Lam:V4_0(x), V(0'))
gen_S:0'5_0(0) ⇔ 0'
gen_S:0'5_0(+(x, 1)) ⇔ S(gen_S:0'5_0(x))
No more defined symbols left to analyse.
(24) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(n1) was proven with the following lemma:
eqTerm(gen_App:Lam:V4_0(+(1, n510_0)), gen_App:Lam:V4_0(n510_0)) → False, rt ∈ Ω(1 + n5100)
(25) BOUNDS(n^1, INF)
(26) Obligation:
Innermost TRS:
Rules:
subst(
x,
a,
App(
e1,
e2)) →
mkapp(
subst(
x,
a,
e1),
subst(
x,
a,
e2))
subst(
x,
a,
Lam(
var,
exp)) →
subst[True][Ite](
eqTerm(
x,
V(
var)),
x,
a,
Lam(
var,
exp))
red(
App(
e1,
e2)) →
red[Let](
App(
e1,
e2),
red(
e1))
red(
Lam(
int,
term)) →
Lam(
int,
term)
subst(
x,
a,
V(
int)) →
subst[Ite](
eqTerm(
x,
V(
int)),
x,
a,
V(
int))
red(
V(
int)) →
V(
int)
eqTerm(
App(
t11,
t12),
App(
t21,
t22)) →
and(
eqTerm(
t11,
t21),
eqTerm(
t12,
t22))
eqTerm(
App(
t11,
t12),
Lam(
i2,
l2)) →
FalseeqTerm(
App(
t11,
t12),
V(
v2)) →
FalseeqTerm(
Lam(
i1,
l1),
App(
t21,
t22)) →
FalseeqTerm(
Lam(
i1,
l1),
Lam(
i2,
l2)) →
and(
!EQ(
i1,
i2),
eqTerm(
l1,
l2))
eqTerm(
Lam(
i1,
l1),
V(
v2)) →
FalseeqTerm(
V(
v1),
App(
t21,
t22)) →
FalseeqTerm(
V(
v1),
Lam(
i2,
l2)) →
FalseeqTerm(
V(
v1),
V(
v2)) →
!EQ(
v1,
v2)
mklam(
V(
name),
e) →
Lam(
name,
e)
lamvar(
Lam(
var,
exp)) →
V(
var)
lambody(
Lam(
var,
exp)) →
expisvar(
App(
t1,
t2)) →
Falseisvar(
Lam(
int,
term)) →
Falseisvar(
V(
int)) →
Trueislam(
App(
t1,
t2)) →
Falseislam(
Lam(
int,
term)) →
Trueislam(
V(
int)) →
Falseappe2(
App(
e1,
e2)) →
e2appe1(
App(
e1,
e2)) →
e1mkapp(
e1,
e2) →
App(
e1,
e2)
lambdaint(
e) →
red(
e)
and(
False,
False) →
Falseand(
True,
False) →
Falseand(
False,
True) →
Falseand(
True,
True) →
True!EQ(
S(
x),
S(
y)) →
!EQ(
x,
y)
!EQ(
0',
S(
y)) →
False!EQ(
S(
x),
0') →
False!EQ(
0',
0') →
Truered[Let][Let](
e,
Lam(
var,
exp),
a) →
red(
subst(
V(
var),
a,
exp))
subst[True][Ite](
False,
x,
a,
Lam(
var,
exp)) →
mklam(
V(
var),
subst(
x,
a,
exp))
red[Let][Let](
e,
App(
t1,
t2),
e2) →
App(
App(
t1,
t2),
e2)
red[Let][Let](
e,
V(
int),
e2) →
App(
V(
int),
e2)
red[Let](
App(
e1,
e2),
f) →
red[Let][Let](
App(
e1,
e2),
f,
red(
e2))
subst[True][Ite](
True,
x,
a,
e) →
esubst[Ite](
False,
x,
a,
e) →
esubst[Ite](
True,
x,
a,
e) →
aTypes:
subst :: App:Lam:V → App:Lam:V → App:Lam:V → App:Lam:V
App :: App:Lam:V → App:Lam:V → App:Lam:V
mkapp :: App:Lam:V → App:Lam:V → App:Lam:V
Lam :: S:0' → App:Lam:V → App:Lam:V
subst[True][Ite] :: False:True → App:Lam:V → App:Lam:V → App:Lam:V → App:Lam:V
eqTerm :: App:Lam:V → App:Lam:V → False:True
V :: S:0' → App:Lam:V
red :: App:Lam:V → App:Lam:V
red[Let] :: App:Lam:V → App:Lam:V → App:Lam:V
subst[Ite] :: False:True → App:Lam:V → App:Lam:V → App:Lam:V → App:Lam:V
and :: False:True → False:True → False:True
False :: False:True
!EQ :: S:0' → S:0' → False:True
mklam :: App:Lam:V → App:Lam:V → App:Lam:V
lamvar :: App:Lam:V → App:Lam:V
lambody :: App:Lam:V → App:Lam:V
isvar :: App:Lam:V → False:True
True :: False:True
islam :: App:Lam:V → False:True
appe2 :: App:Lam:V → App:Lam:V
appe1 :: App:Lam:V → App:Lam:V
lambdaint :: App:Lam:V → App:Lam:V
S :: S:0' → S:0'
0' :: S:0'
red[Let][Let] :: App:Lam:V → App:Lam:V → App:Lam:V → App:Lam:V
hole_App:Lam:V1_0 :: App:Lam:V
hole_S:0'2_0 :: S:0'
hole_False:True3_0 :: False:True
gen_App:Lam:V4_0 :: Nat → App:Lam:V
gen_S:0'5_0 :: Nat → S:0'
Lemmas:
!EQ(gen_S:0'5_0(n7_0), gen_S:0'5_0(+(1, n7_0))) → False, rt ∈ Ω(0)
Generator Equations:
gen_App:Lam:V4_0(0) ⇔ V(0')
gen_App:Lam:V4_0(+(x, 1)) ⇔ App(gen_App:Lam:V4_0(x), V(0'))
gen_S:0'5_0(0) ⇔ 0'
gen_S:0'5_0(+(x, 1)) ⇔ S(gen_S:0'5_0(x))
No more defined symbols left to analyse.
(27) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(1) was proven with the following lemma:
!EQ(gen_S:0'5_0(n7_0), gen_S:0'5_0(+(1, n7_0))) → False, rt ∈ Ω(0)
(28) BOUNDS(1, INF)